poss:(ES{i}Prop{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss)Prop{i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss)Prop{i'}), Rs:(TTProp{i'}).
(Trans _1,_2:possible-event{i:l}(poss). R(_1,_2))
 ma-knows{i:l}
 ma-knows(poss; i; T; s; P; Rs; R)
 ma-knows{i:l}
 ma-knows(poss; i; T; s; (e.es-knows{i:l}(poss; R; P; e)); Rs; R) 

latex

Definitions	t  T, P  Q, x:A. B(x), K(P)@e, Type, Prop, ES, x:AB(x), Id, PossibleEvent(poss), f(a), x,y. t(x;y), Trans x,y:T. E(x;y), poss-consistent(i;T;s;ev;R), Atom$n, x:AB(x), A & B, Ki(P)@s
Lemmas	poss-consistent wf, es-knows wf, trans wf, possible-event wf, Id wf, event system wf, es-knows-knows